\begin{landscape}
\chapter{Codice del Software}

\subsection{main.ml}
\begin{lstlisting}
let source_filename, reduce =
  let reduce_ref = ref false in
  let source_ref = ref None in
  let set_source_file s = source_ref := Some s in
  let _ =
    Arg.parse
      ["--reduce", Arg.Set reduce_ref, " Reduce normal form";
       "--", Arg.Rest set_source_file, " Stop interpreting arguments"]
      set_source_file
      "Usage: minimize OPTIONS filename"
  in
    match !source_ref with
	None -> assert false (* ERROR *)
      | Some s -> s, !reduce_ref

let string_of_state a p =
  Printf.sprintf "q_{%d}" (Builder.A.get_state_index a p)

let string_of_simple_nf_state a p =
  Printf.sprintf "q_{%d}" (Builder.A_fnr.get_state_index a p)

let string_of_state_min a pset =
  if Builder.A_fnr.StateSet.is_empty pset then
    "\\emptyset"
  else
    "\\{" ^ String.concat "," (List.map (string_of_simple_nf_state a) (Builder.A_fnr.StateSet.elements pset)) ^ "\\}"

let string_of_state_set a pset =
  if Builder.A.StateSet.is_empty pset then
    "\\emptyset"
  else
    "\\{" ^ String.concat "," (List.map (string_of_state a) (Builder.A.StateSet.elements pset)) ^ "\\}"

let string_of_action action =
  let name = String.sub action 1 (String.length action - 1) in
    match action.[0] with
	'?' -> name
      | '!' -> "\\overline{" ^ name ^ "}"
      | _ -> assert false (* IMPOSSIBLE *)

let string_of_transition =
  function
      Automaton.Transition.Tau -> "\\tau"
    | Automaton.Transition.Action action -> string_of_action action

let string_of_ready_set rset =
  if Builder.A.ReadySet.is_empty rset then
    "\\emptyset"
  else
    "\\{" ^ String.concat "," (List.map string_of_action (Builder.A.ReadySet.elements rset)) ^ "\\}"

let string_of_acceptance_set aset =
  if Builder.A.AcceptanceSet.is_empty aset then
    "\\emptyset"
  else
    "\\{" ^ String.concat "," (List.map string_of_ready_set (Builder.A.AcceptanceSet.elements aset)) ^ "\\}"

let string_of_nf_state a (pset, aset) =
  "(" ^ string_of_state_set a pset ^ "," ^ string_of_acceptance_set aset ^ ")"

let make_graph to_graph a name =
  let ch = open_out (name ^ ".dot") in
    to_graph ch a name;
    close_out ch

let _ =
  let basename = Filename.basename source_filename in
  let name = Filename.chop_extension basename in
  let lexbuf = Lexing.from_channel (open_in source_filename) in
  let activity = Parser.main Lexer.token lexbuf in
  let t0 = Sys.time () in
  let a = Builder.make_automaton activity in
  let t1 = Sys.time () in
  let q0, b = Builder.make_automaton_fnr reduce a activity in
  let t2 = Sys.time () in
  let r0, c = Builder.minimize b q0 in
  let t3 = Sys.time () in
    Printf.printf "\
building     : %.3fs (%d states)\n\
normal form  : %.3fs (%d states)\n\
minimization : %.3fs (%d states)\n"
      (t1 -. t0) (Builder.A.size a)
      (t2 -. t1) (Builder.A_fnr.size b)
      (t3 -. t2) (Builder.A_min.size c);
    make_graph
      (Builder.A.to_graph "circle" (string_of_state a) string_of_transition)
      a (name ^ ".A");
    make_graph
      (Builder.A_fnr.to_graph "circle" (string_of_simple_nf_state b) string_of_transition)
      b (name ^ ".B");
    make_graph
      (Builder.A_min.to_graph "circle" (string_of_state_min b) string_of_transition)
      c (name ^ ".C");
    flush stdout
\end{lstlisting}

\subsection{lexer.mll}
\begin{lstlisting}

{
 open Parser
}

let carattere = ['a'-'z' 'A'-'Z' '0'-'9' '#' '_' '-']

rule token = parse

eof			{EOL}
|['\t' ' ' '\n']	{token lexbuf}
|"empty"		{EMPTY}
|"sequence"		{SEQUENCE}
|"repeat"               {REPEAT}
|"while"		{WHILE}
|"if"			{IF}
|"flow"			{FLOW}
|"pick"			{PICK}
|"?<"(carattere* as s)'>'	{ AZIONE("?" ^ s)}
|"!<"(carattere* as s)'>'	{ AZIONE("!" ^ s)}
|'{'			{OPENGRAF}
|'}'			{CLOSEGRAF}
|_	{Printf.printf "Carattere '%s' non riconosciuto\n" (Lexing.lexeme lexbuf); token lexbuf}

\end{lstlisting}

\subsection{parser.mly}
\begin{lstlisting}
%{
let fold_activities f al = List.fold_right f al
let fold_if = List.fold_left Contract.mk_if
%}

%token <string> AZIONE
%token OPENGRAF CLOSEGRAF EOL 
%token EMPTY SEQUENCE REPEAT WHILE IF FLOW PICK

%start main
%type <Contract.activity> main
%%

main:
	activity EOL		{$1}
;

activity:
	 EMPTY						{Contract.One}
	|AZIONE						{Contract.Action($1)}
	|SEQUENCE OPENGRAF activity_list CLOSEGRAF	{fold_activities Contract.mk_sequence $3 Contract.One}
	|REPEAT OPENGRAF activity CLOSEGRAF             {Contract.Repeat $3}
	|WHILE OPENGRAF activity CLOSEGRAF		{Contract.While($3)}
	|IF OPENGRAF activity activity_list CLOSEGRAF	{fold_if $3 $4}
	|FLOW OPENGRAF activity_list CLOSEGRAF 		{fold_activities Contract.mk_flow $3 Contract.One}
	|PICK OPENGRAF activity_list CLOSEGRAF 		{fold_activities Contract.mk_pick $3 Contract.Zero}
;

activity_ne_list:
	 activity {[$1]} 
	|activity activity_ne_list {$1::$2}
;

activity_list:
	   {[]}
	|activity_ne_list {$1}
;
\end{lstlisting}

\subsection{automaton.ml}
\begin{lstlisting}

module Transition =
struct
  type t = Tau | Action of string
  let compare = Pervasives.compare
  let string_of =
  function
      Tau -> "-"
    | Action s -> s
end

module TransitionSet = Set.Make(Transition)

module Make =
  functor (State : Set.OrderedType) ->
    struct
      type state_t =
	  { state : State.t;
	    index : int;
	    mutable next : (Transition.t * state_t) list;
	  }

      module HashedState =
      struct
	type t = State.t
	let equal x y = State.compare x y = 0
	let hash = Hashtbl.hash
      end

      module StateMap = Hashtbl.Make(HashedState)

      module StateSet = Set.Make(State)

      type t =
	  { mutable next_index : int;
	    mutable state_map : state_t StateMap.t;
	  }

      let make () =
	{ next_index = 0;
	  state_map = StateMap.create 1023;
	}

      let mk_state v index =
	{ state = v;
	  index = index;
	  next = [];
	}

      let get_states a =
	let pl = ref [] in
	  StateMap.iter
	    (fun p _ -> pl := p :: !pl)
	    a.state_map;
	  !pl

      let size a = List.length (get_states a)

      let get_internal_state a = StateMap.find a.state_map
      let get_external_state s = s.state

      let get_state a p =
	try
	  (false, get_internal_state a p)
	with
	    Not_found ->
	      let s = mk_state p a.next_index in
		a.next_index <- a.next_index + 1;
		StateMap.add a.state_map p s;
		(true, s)

      let make_state a p = fst (get_state a p)

      let get_state_index a p = (get_internal_state a p).index

      let get_state_transitions a p =
	let s = get_internal_state a p in
	  List.map
	    (fun (t, s') -> t, get_external_state s')
	    s.next

      let add_transition a p t p' =
	let s = get_internal_state a p
	and s' = get_internal_state a p' in
	  s.next <- (t, s') :: s.next

      let to_graph default_node_shape string_of_state string_of_transition ch a name =
	Printf.fprintf ch "digraph \"%s\" {\n" name;
	Printf.fprintf ch "  d2tdocpreamble = \"\\usetikzlibrary{automata}\";\n";
	Printf.fprintf ch "  d2tfigpreamble = \"\\tikzstyle{every state}=[draw=blue!50,very thick,fill=blue!20]\"\n";
(* 	Printf.fprintf ch "  node [shape=%s,fixedsize=true,width=0.3,height=0.3];\n" default_node_shape; *)
	Printf.fprintf ch "  node [style=state];\n";
	Printf.fprintf ch "  edge [lblstyle=auto];\n";
	Printf.fprintf ch "  q0 [style=state,initial];\n";
	StateMap.iter
	  (fun _ s ->
	     Printf.fprintf ch "  q%d [label=\"q%d\",texlbl=\"$%s$\"];\n"
	       s.index s.index
	       (string_of_state (get_external_state s))
	  )
	  a.state_map;
	StateMap.iter
	  (fun _ s ->
	     List.iter
	       (fun (t, s') ->
		  Printf.fprintf ch "  q%d -> q%d [label=\"%s\",texlbl=\"$%s$\"];\n"
		    s.index s'.index
		    (Transition.string_of t)
		    (string_of_transition t)
	       )
	       s.next
	  )
	  a.state_map;
	Printf.fprintf ch "}\n"

      let pp string_of_state string_of_transition a =
	StateMap.iter
	  (fun p s ->
	    List.iter
	      (fun (t, s') ->
		Printf.printf "%s --%s--> %s\n" (string_of_state p) (string_of_transition t) (string_of_state (get_external_state s'))
	      )
	      s.next
	  )
	  a.state_map

      let reachable a t s =
	let s' = get_internal_state a s in
	  List.fold_right
	    (fun (_, s'') -> StateSet.add (get_external_state s''))
	    (List.filter (fun (t', _) -> t = t') s'.next)
	    StateSet.empty

      let reachable_set a t sset =
	StateSet.fold (fun s -> StateSet.union (reachable a t s)) sset StateSet.empty

      let tau_closure_set a =
	FunAux.limit StateSet.equal (fun pset -> StateSet.union pset (reachable_set a Transition.Tau pset))

      let tau_closure a p = tau_closure_set a (StateSet.singleton p)

	(*Funtore ReadySet*)
      module OrderedAction = 
	struct
 	 type t = string
  	 let compare = Pervasives.compare
	 let string_of s = s
      end

	(*Modulo che utilizzo per la costruzione di ActionSet contenenti azioni*)
      module ReadySet = Set.Make(OrderedAction)

      let succ a p =
	let s = get_internal_state a p in
	  List.fold_right
	    (fun (t, _) -> TransitionSet.add t)
	    s.next
	    TransitionSet.empty

      let succ_set a pset =
	StateSet.fold (fun p -> TransitionSet.union (succ a p)) pset TransitionSet.empty

      let ready_set a s = 
	let s' = get_internal_state a s in
	  List.fold_right
	    (function
		 (Transition.Action a, _) -> ReadySet.add a
	       | (Transition.Tau, _) -> fun x -> x)
	    (s'.next)
	    ReadySet.empty	

      let ready_set_set a sset =
  	StateSet.fold (fun s -> ReadySet.union (ready_set a s)) sset ReadySet.empty

      (*Funtore AcceptanceSet*)
      module OrderedReadySet = 
      struct
        type t = ReadySet.t
        let compare = ReadySet.compare
      end

      (*Modulo che utilizzo per la costruzione di AcceptanceSet contenenti ReadySet*)
      module AcceptanceSet = Set.Make(OrderedReadySet)

      let is_stable a p =
	StateSet.is_empty (reachable a Transition.Tau p)

      (*Funzione che dato in ingresso un automa e uno stato mi calcola l'AcceptanceSet dello stato in questo modo:
	- calcola la tau-closure dello stato in input;
	- calcola l'acceptance-set come unione dei ready-set degli stati tau-closed da quello di input*)
      let acceptance_set a p =
        StateSet.fold
          (fun q -> AcceptanceSet.add (ready_set a q))
          (StateSet.filter (is_stable a) (tau_closure a p))
          AcceptanceSet.empty

      let acceptance_set_set a sset = 
       StateSet.fold (fun s -> AcceptanceSet.union (acceptance_set a s)) sset AcceptanceSet.empty

     (*Funzione che dato in ingresso un automa e uno stato ti calcola l'AcceptanceSet minimo dello stato in input*)
      let min_acceptance_set aset =
	AcceptanceSet.filter
          (fun rset -> 
	     AcceptanceSet.for_all
	       (fun rset' -> 
		  not (ReadySet.subset rset' rset) || ReadySet.equal rset' rset) aset)
          aset

     (*Funzione che dato un AcceptanceSet calcola l'unione dei ReadySet*)
      let union_acceptance_set aset = 
	AcceptanceSet.fold ReadySet.union aset ReadySet.empty  

     (*Funzione che dato in ingresso un automa e uno stato calcola l'AcceptanceSet caratteristico dello stato in input*)
      let car_acceptance_set aset = 
	let min_aset = min_acceptance_set aset in
	let uset = union_acceptance_set aset in
          if ReadySet.equal uset (union_acceptance_set min_aset) then
            min_aset
          else 
            AcceptanceSet.add uset min_aset 

      let sat_acceptance_set aset =
	let close_union aset =
	  AcceptanceSet.fold
	    (fun rset aset' ->
	      AcceptanceSet.fold
		(fun rset' -> AcceptanceSet.add (ReadySet.union rset rset'))
		aset
		aset'
	    )
	    aset
	    AcceptanceSet.empty
	in
	  close_union (car_acceptance_set aset)
    end
\end{lstlisting}
    
\subsection{builder.ml}
\begin{lstlisting}
(*Funtore automa di partenza i cui stati sono activity*)
module OrderedActivity =
struct
  type t = Contract.activity
  let compare = Pervasives.compare
end

(*Automa di partenza*)
module A = Automaton.Make(OrderedActivity)

(*Funzione per denotare quando un'attività è nello stato finale*)
let rec is_final =
  function
      Contract.One
    | Contract.Repeat _ -> true
    | Contract.Zero
    | Contract.Action _
    | Contract.While _
    | Contract.If _ -> false
    | Contract.Sequence (a, b)
    | Contract.Flow (a, b) -> is_final a && is_final b
    | Contract.Pick (a, b) -> is_final a || is_final b

(*Funzione che data un'attività definisce il sistema di transizioni associato a tale attività*)
let rec all_transitions =
  function
      Contract.Zero
    | Contract.One -> []
    | Contract.Action (n) -> [Automaton.Transition.Action n, Contract.One]
    | Contract.Sequence (a, b) ->
	List.map (fun (t, a') -> t, Contract.Sequence (a', b)) (all_transitions a)
	@ (if is_final a then all_transitions b else [])
    | Contract.Repeat a as a' ->
	List.map (fun (t, a'') -> t, Contract.Sequence (a'', a')) (all_transitions a)
    | Contract.While a as a' ->
	[Automaton.Transition.Tau, Contract.One;
	 Automaton.Transition.Tau, Contract.Sequence (a, a')]
    | Contract.If (a, b) -> [Automaton.Transition.Tau, a; Automaton.Transition.Tau, b]
    | Contract.Flow (a, b) ->
	List.map (fun (t, a') -> t, Contract.Flow (a', b)) (all_transitions a)
	@ List.map (fun (t, b') -> t, Contract.Flow (a, b')) (all_transitions b)
    | Contract.Pick (a, b) ->
	let is_tau_transition (t, _) = t = Automaton.Transition.Tau in
	let tau_at, visible_at = List.partition is_tau_transition (all_transitions a)
	and tau_bt, visible_bt = List.partition is_tau_transition (all_transitions b) in
	  List.map (fun (tau, a') -> tau, Contract.Pick (a', b)) tau_at
	  @ List.map (fun (tau, b') -> tau, Contract.Pick (a, b')) tau_bt
	  @ visible_at @ visible_bt

(*Funzione che costruisce imperativamente l'automa di partenza*)
let make_automaton s0 =
  let a = A.make () in
  let rec aux =
    function
	[] -> ()
      | s :: sl ->
	  begin
	    let rec add_transitions sl' =
	      function
		  [] -> aux sl'
		| (t, s') :: at ->
		    let is_new = A.make_state a s' in
		      A.add_transition a s t s';
		      if is_new then
			add_transitions (s' :: sl') at
		      else
			add_transitions sl' at
	    in
	      add_transitions sl (all_transitions s)
	  end
  in
  let _ = A.make_state a s0 in
    aux [s0];
    a

(*Funtore automa forma normale ridotta i cui stati sono coppie (stati,acceptance-set)*)
module OrderedState_fnr =
struct
  type t = A.StateSet.t * A.AcceptanceSet.t
  let compare (pset, aset) (qset, bset) =
    let c1 = A.StateSet.compare pset qset
    and c2 = A.AcceptanceSet.compare aset bset in
      if c1 = 0 then c2 else c1
end

(*Automa in forma normale ridotta*)
module A_fnr = Automaton.Make(OrderedState_fnr)

(*Funzione che costruire imperativamente l'automa in forma normale ridotta*)
let make_automaton_fnr reduce a p0 = 
  let my_acceptance_set =
    if reduce then A.car_acceptance_set else A.sat_acceptance_set
  in
  let b = A_fnr.make () in
  let rec aux =
    function
	[] -> ()
      | ((pset, aset) as q) :: ql when A.AcceptanceSet.cardinal aset = 1 ->
	  A.ReadySet.iter
	    (fun action ->
	      let pset' = 
		A.StateSet.fold 
		  (fun p -> A.StateSet.union (A.reachable_set a (Automaton.Transition.Action action) (A.tau_closure a p)))
		  pset
		  A.StateSet.empty
	      in
	      let aset' = my_acceptance_set (A.acceptance_set_set a pset') in
	      let q' = (pset', aset') in
	      let is_new = A_fnr.make_state b q' in
		A_fnr.add_transition b q (Automaton.Transition.Action action) q';
		if is_new then aux (q' :: ql) else aux ql
	    )
	    (A.AcceptanceSet.choose aset)
      | ((pset, aset) as q) :: ql ->
	  assert (A.AcceptanceSet.cardinal aset > 1);
	  A.AcceptanceSet.iter
	    (fun rset ->
	      let q' = (pset, A.AcceptanceSet.singleton rset) in
	      let is_new = A_fnr.make_state b q' in
		A_fnr.add_transition b q Automaton.Transition.Tau q';
		if is_new then aux (q' :: ql) else aux ql
	    )
	    aset
  in
  let q0 = (A.StateSet.singleton p0, my_acceptance_set (A.acceptance_set a p0)) in
  let _ = A_fnr.make_state b q0 in
    aux [q0];
    (q0, b)

module OrderedState_min =
struct
  type t = A_fnr.StateSet.t
  let compare = A_fnr.StateSet.compare
end

(*Automa in forma normale ridotta*)
module A_min = Automaton.Make(OrderedState_min)

let minimize a p0 =
  let states = A_fnr.get_states a in
  let iter_pairs f =
    let rec aux =
      function
	  [] -> ()
	| p :: pl -> List.iter (f p) pl; aux pl
    in
      aux states
  in
  let dist = ref [] in
  let is_distinguishable p q =
    List.exists
      (fun (p', q') ->
	(OrderedState_fnr.compare p p' = 0 && OrderedState_fnr.compare q q' = 0)
      || (OrderedState_fnr.compare p q' = 0 && OrderedState_fnr.compare q p' = 0))
      !dist
  in
    iter_pairs
      (fun ((_, aset) as p) ((_, bset) as q) ->
	 if not (A.AcceptanceSet.equal aset bset) then
	   dist := (p, q) :: !dist
      );
    let rec aux () =
      let new_dist = ref [] in
	iter_pairs
	  (fun p q ->
	     if not (is_distinguishable p q) then
	       let rset = A.AcceptanceSet.choose (snd p) in
		 if
		   (A_fnr.StateSet.exists
		      (fun p' ->
			 A_fnr.StateSet.exists
			   (fun q' -> is_distinguishable p' q')
			   (A_fnr.reachable a Automaton.Transition.Tau q)
		      )
		      (A_fnr.reachable a Automaton.Transition.Tau p))
		   ||
		     (A.ReadySet.exists
			(fun action ->
			   A_fnr.StateSet.exists
			     (fun p' ->
				A_fnr.StateSet.exists
				  (fun q' -> is_distinguishable p' q')
				  (A_fnr.reachable a (Automaton.Transition.Action action) q)
			     )
			     (A_fnr.reachable a (Automaton.Transition.Action action) p)
			)
			rset)
		 then
		   new_dist := (p, q) :: !new_dist
	  );
	if !new_dist <> [] then
	  begin
	    dist := !new_dist @ !dist;
	    aux ()
	  end
    in
      aux ();
      (*
      List.iter
	(fun (p, q) ->
	  Printf.printf "(%d, %d)\n" (A_fnr.get_state_index a p)
	    (A_fnr.get_state_index a q)
	)
	!dist;
      *)
      let add_to_partition partl p =
	let rec aux =
	  function
	      [] -> [A_fnr.StateSet.singleton p]
	    | pset :: partl
		when not (A_fnr.StateSet.exists (is_distinguishable p) pset) ->
		(A_fnr.StateSet.add p pset) :: partl
	    | pset :: partl -> pset :: aux partl
	in
	  aux partl
      in
      let partition = List.fold_left add_to_partition [] states in
      let get_partition p =
	try
	  List.find (A_fnr.StateSet.mem p) partition
	with
	    Not_found -> assert false
      in
      let b = A_min.make () in
      let add_transition p t q =
	let p' = get_partition p
	and q' = get_partition q in
	let _ = A_min.make_state b p'
	and _ = A_min.make_state b q' in
	  A_min.add_transition b p' t q'
      in
	List.iter
	  (fun pset ->
	    let p = A_fnr.StateSet.choose pset in
	      List.iter
		(fun t ->
		  let qset = A_fnr.reachable_set a t pset in
		    match t with
			Automaton.Transition.Tau ->
			  A_fnr.StateSet.iter (add_transition p t) qset
		      | Automaton.Transition.Action _ ->
			  let q = A_fnr.StateSet.choose qset in
			    add_transition p t q
	      )
	      (Automaton.TransitionSet.elements (A_fnr.succ_set a pset))
	  )
	  partition;
	(get_partition p0, b)
\end{lstlisting}
	
\subsection{funAux.ml}
\begin{lstlisting}
(*Calcolo il punto fisso di una funzione*)

let limit eq f =
  let rec aux x =
    let x' = f x in
      if eq x x' then
	x'
      else
	aux x'
  in
    aux
\end{lstlisting}

\subsection{contract.ml}
\begin{lstlisting}
(* Definizione Datatype per le Attività dei Servizi Web *)
type activity = 
    Zero
  | One
  | Action of string
  | Sequence of activity * activity
  | Repeat of activity
  | While of activity
  | If of activity * activity
  | Flow of activity * activity	
  | Pick of activity * activity

let mk_sequence a1 a2 = Sequence (a1, a2)
let mk_if a1 a2 = If (a1, a2)
let mk_flow a1 a2 = Flow (a1, a2)
let mk_pick a1 a2 = Pick (a1, a2)

let rec pp = 
  function
      Zero -> "Zero"
    | One -> "One"
    | Action(a) -> "Action(" ^ a ^ ")"
    | Sequence(a,b) -> "Sequence(" ^ (pp a) ^ ", " ^ (pp b) ^ ")" 
    | Repeat a -> "Repeat(" ^ pp a ^ ")"
    | While(a) -> "While(" ^ (pp a) ^ ")"
    | If(a,b) -> "If(" ^ (pp a) ^ ", " ^ (pp b) ^ ")"
    | Flow(a,b) -> "Flow(" ^ (pp a) ^ ", " ^ (pp b) ^ ")"
    | Pick(a,b) -> "Pick(" ^ (pp a) ^ ", " ^ (pp b) ^ ")"
    
\end{lstlisting}
\end{landscape}

